$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $L$:($a$:$A$ fp$\rightarrow$ $B$($a$) List). $\oplus$($L$) $\in$ $a$:$A$ fp$\rightarrow$ $B$($a$)